Iof proof for Lemma gen hyp tp:
1. A : Type
2. e : A
3. H : A
Type
4. z : H(e)
z 
0
by (%S%
\p.
\plet UA = get_term_arg `UA` p
\pin let A = get_term_arg `A` p
\pinin let e = get_term_arg `e` p
\pin let x = get_term_arg `x` p
\pin
\piAssertL
\piAsse[mk_member_term UA A
\piAs;mk_member_term A e
\piAs;mk_all_term (dv x) A (mk_member_term
\piAs;mk_all_term (dv x) A (mk_meUA (mk_equal_term A e x))
\piAs]
\pip)
\p1: .....assertion..... NILNIL
\p1:
A 
Type
\p2: .....assertion..... NILNIL
\p2: 5. A
Type
\p2:
e A
\p3: .....assertion..... NILNIL
\p3: 5. A
Type
\p3: 6. e
A
\p3:
x:A. (e = x) Type
\p4:
\p4: 5. A
Type
\p4: 6. e
A
\p4: 7.
x:A. (e = x) Type
\p4:
z 0
\p.